Postée il y a 4 heures
Titre: Fondements des logiques CCSA
Les logiques CCSA sont utilisées pour raisonner sur les messages et protocoles cryptographiques. Elles ont émergé des travaux pionniers de Bana et Comon [1] basés sur la logique du premier ordre, qui a progressivement évolué vers une logique CCSA du second ordre [2], mise en œuvre dans l'assistant de preuve Squirrel [3]. Dans ces logiques, des constantes spéciales appelées noms sont utilisées pour modéliser des familles d'échantillonnages aléatoires, utilisées par exemple pour modéliser des clés cryptographiques ou des nonces. Les hypothèses cryptographiques (c'est-à-dire, la sécurité de jeux particuliers impliquant des primitives cryptographiques) sont alors exprimées sous forme de schémas d'axiomes - formellement, ces axiomes peuvent être générés à partir des jeux cryptographiques par bi-déduction.
L'objectif global de cette thèse sera d'élargir le champ d'application des logiques CCSA, en considérant de nouvelles variantes dans cet espace conceptuel, et de mieux comprendre leur théorie des preuves. Une partie du travail consistera donc à concevoir de nouvelles logiques avec une sémantique appropriée. Une autre partie consistera à étudier les propriétés clés de ces logiques, telles que la compacité, la décidabilité... et à concevoir des systèmes de preuves pour lesquels des résultats de complétude peuvent être obtenus. Certains de ces résultats peuvent avoir un impact pratique dans l'assistant de preuve Squirrel, qui pourrait devenir plus expressif ou bénéficier de nouvelles capacités de raisonnement automatisé.
Un premier objectif sera d'équiper les logiques CCSA de quantification sur des noms frais. La logique enrichie devrait permettre d'écrire des choses telles que « pour tout x, frais n, n - x » qui devraient être valides, car un nom n qui est frais par rapport à x a une probabilité négligeable d'entrer en collision avec ce nom. Ce quantificateur serait utile pour exprimer des axiomes cryptographiques mais aussi dans des lemmes intermédiaires où les utilisateurs de Squirrel introduisent typiquement des noms frais : au lieu des noms frais codés en dur actuels, un traitement logique approprié apportera plus de flexibilité, par exemple choisir le nom frais en fonction du contexte, ou le renommer, tant que la fraîcheur est assurée. Ce projet, dont les premières étapes sont actuellement en cours d'investigation dans le cadre du stage de M2 de Thibaut Antoine, s'inspirera à la fois de la logique nominale [5] et de la quantification générique [5] et de sa sémantique catégorielle [7]. Une fois terminé, la logique devrait être conservatrice par rapport à la logique CCSA du second ordre existante, et venir avec un calcul séquentiel naturel.
En s'appuyant sur les résultats de l'objectif précédent, un deuxième but sera d'étendre les résultats de complétude obtenus pour les logiques modales CCSA de [0] à un cadre incluant l'indistinguabilité computationnelle. Cette question est triviale sans noms frais, mais devient intéressante une fois qu'ils peuvent être pris en compte.
Au-delà de ces deux premiers objectifs, le doctorant abordera des questions plus larges. Il serait souhaitable d'obtenir des résultats de complétude dans le cadre du premier ordre (ou même du second ordre). Nous nous attendons également à ce que la restriction technique aux bandes finies dans la sémantique de nos logiques cause des difficultés récurrentes ; il serait naturel d'explorer comment elle pourrait être levée. Enfin, le travail ne devrait pas rester uniquement attaché à ses motivations originales dans les logiques CCSA : les questions abordées ici ne sont même pas spécifiques à la cryptographie, mais traitent de questions larges sur les probabilités et la logique, qui ont été abordées dans des travaux classiques et récents [8,9].
[0] Antoine. "Propositional Logics of Overwhelming Truth". CSL 2025.
[1] Bana, Comon. "A computationally complete symbolic attacker for equivalence properties." CCS 2014.
[2] Baelde, Koutsos, Lallemand. "A higher-order indistinguishability logic for cryptographic reasoning." LICS 2023.
[3] Baelde et al. "An interactive prover for protocol verification in the computational model." S&P 2021.
[4] Baelde et al. "Foundations for Cryptographic Reductions in CCSA Logics." CCS 2024.
[5] Pitts. "Nominal logic, a first order theory of names and binding." Information and Computation 2003.
[6] Miller, Tiu. "A proof theory for generic judgments." ACM TOCL 2005.
[7] Goubault-Larrecq. "A semantics for nabla." MSCS 2019.
[8] Geiger, Paz, Pearl. "Axioms and algorithms for inferences involving probabilistic independence." Information and Computation 1991.
[9] Li et al. "A Nominal Approach to Probabilistic Separation Logic." LICS 2024.